Nuprl Lemma : add_mono_wrt_eq_rw
13,42
postcript
pdf
a
,
b
,
n
:
. {(
a
=
b
)
(
a
+
n
=
b
+
n
)}
latex
Up
int
2
,
int
2
Definitions
{
T
}
Lemmas
add
mono
wrt
eq
origin
a, b, n:
. {(a = b) 
(a+n = b+n)} a, b, n:. {(a = b) (a+n = b+n)}